\begin{tabbing} (\=(((RecUnfold `nth\_tl` 0) \+ \\[0ex]CollapseTHEN ((((if (0 \-\\[0ex])\= =0 then SplitOnConclITE else SplitOnHypITE (0))$\cdot$) \+ \\[0ex]CollapseTHEN (Reduce 0))$\cdot$))$\cdot$) \\[0ex] \\[0ex]CollapseTHEN ((Try ((Complete (Auto'))$\cdot$))$\cdot$))$\cdot$ \- \end{tabbing}